#ifndef _PDT_TRAVERSAL_H_
#define _PDT_TRAVERSAL_H_

#include "PDTTraversalIFC.h"

#define olog()  cout<<__FILE__<<":"<<__PRETTY_FUNCTION__<<":"<<__LINE__<<": "
#define elog()  cerr<<__FILE__<<":"<<__PRETTY_FUNCTION__<<":"<<__LINE__<<": "

class PDTCodeGraph;
class PDTNode;
class PDTConst;
class PDTQuantifier;

class PDTEvalTraversal : public Traversal {
    PDTCodeGraph & cg;
    PDTConst ** values;
    unsigned int size;

    private:
    PDTConst * getChildValue(PDTNode & d, unsigned int i) const;

    public:
    bool setValue(PDTNode & d, PDTConst* clone);
    PDTConst * getValue(PDTNode & d) const ;
    PDTConst * getValue(PDTNode * d) const ;

    PDTCodeGraph & getCodeGraph() const {
        return cg;
    }

    PDTEvalTraversal(PDTCodeGraph & aCG);
    virtual ~PDTEvalTraversal();

    // PDTAdd 
    virtual Traversal::RetType post(PDTAdd &);

    // PDTAnd 
    virtual Traversal::RetType post(PDTAnd &);


    // PDTAssert 
    virtual Traversal::RetType post(PDTAssert &);


    // PDTAssign 
    virtual Traversal::RetType beforeChild(PDTAssign & d, unsigned int i);
    virtual Traversal::RetType post(PDTAssign &);


    // PDTBehavior 
    //virtual Traversal::RetType post(PDTBehavior &);
    virtual Traversal::RetType pre(PDTBehavior &);//Skip!

    // PDTBehaviors 
    //virtual Traversal::RetType post(PDTBehaviors &);
    virtual Traversal::RetType pre(PDTBehaviors &);//Skip!

    // PDTBoolConst 
    virtual Traversal::RetType post(PDTBoolConst &);


    // PDTBoolVar 
    virtual Traversal::RetType post(PDTBoolVar &);


    // PDTConstSequence 
    virtual Traversal::RetType post(PDTConstSequence &);


    // PDTDiv 
    virtual Traversal::RetType post(PDTDiv &);


    // PDTEqualBool 
    virtual Traversal::RetType post(PDTEqualBool &);


    // PDTEqualNum 
    virtual Traversal::RetType post(PDTEqualNum &);


    Traversal::RetType enumerateRanges (PDTQuantifier& d, unsigned int varIdx ) ;
    // PDTExist 
    virtual Traversal::RetType pre(PDTExist &);


    // PDTForall 
    virtual Traversal::RetType pre(PDTForall &);


    // PDTFunctionCall 
    virtual Traversal::RetType post(PDTFunctionCall &);

    Traversal::RetType scasize(PDTFunctionCall&);
    Traversal::RetType scchar(PDTFunctionCall&, char ch);
    Traversal::RetType sccharrange(PDTFunctionCall&, char ch1,char ch2);
    Traversal::RetType scalphanum(PDTFunctionCall&);

    // PDTFunctionDec 
    //virtual Traversal::RetType post(PDTFunctionDec &);


    // PDTGreaterThan 
    virtual Traversal::RetType post(PDTGreaterThan &);


    // PDTGreaterThanEqual 
    virtual Traversal::RetType post(PDTGreaterThanEqual &);


    // PDTIfElse 
    virtual Traversal::RetType beforeChild(PDTIfElse & d, unsigned int i);
    virtual Traversal::RetType post(PDTIfElse &);


    // PDTImplies 
    virtual Traversal::RetType beforeChild(PDTImplies& d, unsigned int i);
    virtual Traversal::RetType post(PDTImplies &);


    // PDTIntRange 
    virtual Traversal::RetType post(PDTIntRange &);


    // PDTInvariant 
    virtual Traversal::RetType post(PDTInvariant &);
#if 0
    virtual Traversal::RetType pre(PDTInvariant &){
        return Traversal::Skip;
    }
#endif

    // PDTLessThan 
    virtual Traversal::RetType post(PDTLessThan &);


    // PDTLessThanEqual 
    virtual Traversal::RetType post(PDTLessThanEqual &);


    // PDTListOfStatements 
    //virtual Traversal::RetType post(PDTListOfStatements &);


    // PDTMod 
    virtual Traversal::RetType post(PDTMod &);


    // PDTMult 
    virtual Traversal::RetType post(PDTMult &);


    // PDTNeg 
    virtual Traversal::RetType post(PDTNeg &);


    // PDTNilStatement 
    //virtual Traversal::RetType post(PDTNilStatement &);


    // PDTNot 
    virtual Traversal::RetType post(PDTNot &);


    // PDTNotEqualBool 
    virtual Traversal::RetType post(PDTNotEqualBool &);


    // PDTNotEqualNum 
    virtual Traversal::RetType post(PDTNotEqualNum &);


    // PDTNumConst 
    virtual Traversal::RetType post(PDTNumConst &);


    // PDTNumConstDbl 
    virtual Traversal::RetType post(PDTNumConstDbl &);


    // PDTNumConstInt 
    virtual Traversal::RetType post(PDTNumConstInt &);


    // PDTNumVar 
    virtual Traversal::RetType post(PDTNumVar &);


    // PDTOr 
    virtual Traversal::RetType post(PDTOr &);


    // PDTPair 
    virtual Traversal::RetType post(PDTPair &);


    // PDTPostCondition 
    virtual Traversal::RetType post(PDTPostCondition &);
#if 0
    virtual Traversal::RetType pre(PDTPostCondition &){
        return Traversal::Skip;
    }
#endif


    // PDTPreCondition 
    virtual Traversal::RetType post(PDTPreCondition &);
#if 0
    virtual Traversal::RetType pre(PDTPreCondition &){
        return Traversal::Skip;
    }
#endif


    // PDTProp 
    virtual Traversal::RetType post(PDTProp &);
#if 0
    virtual Traversal::RetType pre(PDTProp &) {
        return Traversal::Skip;
    }
#endif


    // PDTRelation 
    virtual Traversal::RetType post(PDTRelation &);


    // PDTSequence 
    virtual Traversal::RetType post(PDTSequence &);


    // PDTSequenceAccessBool 
    virtual Traversal::RetType post(PDTSequenceAccessBool &);


    // PDTSequenceAccessNum 
    virtual Traversal::RetType post(PDTSequenceAccessNum &);


    // PDTSequenceAssign 
    Traversal::RetType beforeChild(PDTSequenceAssign & d, unsigned int i);
    virtual Traversal::RetType post(PDTSequenceAssign &);


    // PDTSequenceVar 
    virtual Traversal::RetType post(PDTSequenceVar &);


    // PDTSet 
    //virtual Traversal::RetType post(PDTSet &);


    // PDTSetVar 
    //virtual Traversal::RetType post(PDTSetVar &);

    // PDTSubt 
    virtual Traversal::RetType post(PDTSubt &);


    // PDTWhile 
    virtual Traversal::RetType pre(PDTWhile &);


    // PDTXor 
    virtual Traversal::RetType post(PDTXor &);


    // PDTUnresolvedExp 
    virtual Traversal::RetType post(PDTUnresolvedExp &);


    // PDTType 
    //virtual Traversal::RetType post(PDTType &);


    // PDTUnaryNumExpr 
    virtual Traversal::RetType post(PDTUnaryNumExpr &);

};
#endif
